k:Knd. sqequal(islocal(k); (isrcv(k))) 

latex

Definitions	x:A. B(x), islocal(k), b, isrcv(k), isl(x), tt, ff, if b then t else f fi , t  T, Knd, sq_type(T), P  Q, guard(T)
Lemmas	bfalse wf, btrue wf, bool sq, Knd wf